% vim: set fdm=marker:
\section{Pravdivosť a dokázateľnosť}

\begin{definicia}[Logická platnosť formuly]
%%% {{{
    Nech $L$ je jazyk prvého rádu a $A$ je formula jazyka
    $L$. Hovoríme, že formula $A$ je logicky platná,
    označujeme $\models A$,
    ak je splnená v ľubovoľnej realizácii $\mathcal{M}$ jazyka $L$.

    \begin{align*}
        \mathcal{M} & \models A[e] \quad \forall \mathcal{M} \\
        \mathcal{M} & \models A \\
        & \models A
    \end{align*}
%%% }}}    
\end{definicia}

\begin{poznamka}
    Formula $A$ je logicky platná, práve vtedy, keď je pravdivá
    bez ohľadu na realizáciu symbolov jazyka $L$.
\end{poznamka}

\begin{definicia}[Teória]
%%% {{{
    Nech $L$ je jazyk prvého rádu a $T$ je množina formúl
    jazyka $L$. Hovoríme, že $T$ je teória 1. rádu predikátovej logiky
    s jazykom $L$ (t.j. množina formúl $T$ je množina axióm teórie).
%%% }}}
\end{definicia}

\begin{definicia}[Model teórie]
%%% {{{
    Nech $T$ je teória v jazyku $L$, $\mathcal{M}$ je realizácia jazyka $L$.
    Hovoríme, že $\mathcal{M}$ je modelom teórie $T$ (označujeme
    $\mathcal{M} \models T$), ak pre každú formulu $A$
    patriacu $T$ platí $\mathcal{M} \models A$.
%%% }}}
\end{definicia}

\begin{definicia}[Tautologický dôsledok]
%%% {{{
    Hovoríme, že formula $A$ je
    sémantickým/tautologickým dôsledkom (vetou teórie) množiny formúl $T$,
    resp. $A$ je $T$-platná, ak $A$ je splnená v každom modeli teórie $T$.
    Túto skutočnosť označujeme $T \models A$.
%%% }}}
\end{definicia}

\begin{priklad}[Teória ostrého usporiadania]
%%% {{{
    Majme predikát $<$ na množine $\mathbb{N}$, tak, že platí
    \begin{itemize}
    \item[1.] $(\forall x)(\forall y) ((x < y) \implies \neg (y < x))$
        -- asymetrickosť

    \item[2.] $(\forall x)(\forall y)(\forall z) (((x<y) \land (y<z)) \implies
        (x<z))$ -- tranzitívnosť

    \item[3.] $(\forall x)(\forall y)( (x\not=y) \implies ((x<y) \lor (y<x)))$
        -- trichotomickosť
    \end{itemize}
    Ak sú splnené axiómy 1,2, tak daná množina je modelom 
    {\it čiastočného} ostrého. usporiadania. Ak je
    navyše splnená aj axióma 3, množina tvorí teóriu ostrého
    usporiadania.
%%% }}}    
\end{priklad}
\begin{poznamka}
    Pozornému čitateľovi isto neušiel fakt, že sme už raz mali teóriu
    usporiadania a mali sme v nej až 4 axiómy. Poznamenajme, že vtedy
    išlo o teóriu \emph{ne}ostrého usporiadania $\le$ a chýbajúca
    axióma bola
    \begin{equation*}
        (\forall x) (x \le x)
    \end{equation*}
\end{poznamka}

\begin{priklad}[Elementárna aritmetika]
%%% {{{
    Jazyk prvého rádu rozšírme o nasledujúce symboly:
    \begin{itemize}
        \item $0$ -- konštanta (nulárny funkčný symbol),
        \item $S$ -- nasledovník (unárny funkčný symbol), čiže $S(x)=x+1$
        \item $+,*$ -- binárne funkčné symboly
    \end{itemize}
    Axiómy elementárnej aritmetiky:
    \begin{itemize}
        \item[1.] $\neg (S(x) = 0)$
        \item[2.] $(S(x) = S(y)) \implies (x=y)$
        \item[3.] $(x+0) = x$
        \item[4.] $(x+S(y)) = (S(x) + y)$
        \item[5.] $(x * 0) = 0$
        \item[6.] $(x * S(y)) = ((x*y)+x)$
    \end{itemize}
    Zoberme si realizáciu 
        $\mathcal{N}=\langle \mathbb{N}_0,0,S,+,* \rangle$ kde  
        $\mathbb{N}_0 = \{0,1,2,\dots\}$.
        Potom $\mathcal{N}$ je model pre elementárnu aritmetiku,
        zvykne sa označovať aj ako \emph{štandardný model}.
        Takejto aritmetike sa hovorí Robinsonova aritmetika.
        Ak pridáme axiómu indukcie, dostaneme Peanovu aritmetiku.
%%% }}}
\end{priklad}

\begin{poznamka}
    Nevšímajme si nachvíľu axiómy, ale iba relačnú štruktúru
    $\mathcal{N}=\langle \mathbb{N}_0,0,S,+,* \rangle$.
    Zoberme namiesto $S$ konštantu $1$.
    Ciže $\mathcal{N}'=\langle \mathbb{N}_0,0,1,+,* \rangle$.
    $\mathcal{N}'$ realizuje jazyk teórie telies.
    Lenže $\mathcal{N}'$ nie je modelom tohoto jazyka --
    na to, aby daná realizácia bola modelom, muselo by platiť, že
    každá formula $T$ je splnená v danej realizácii. V našom prípade,
    v každom telese platí $\provable \neg (S(S(0))=S(0))$ (inak
    povedané, $2 \ne 1$, ak má teleso charakteristiku viac ako 2,
    v prípade charakteristiky 2 je to $0 \ne 1$). Nuž ale v 
    $\mathcal{N}'$ je splnená formula $S(S(0))=S(0)$, lebo sa
    realizuje ako $1=1$.
\end{poznamka}

\begin{priklad}[Teória grúp]
%%% {{{
    Špeciálne symboly sú $+$ (binárna operácia), $-$ (unárna operácia
    -- inverzný prvok) a $0$ (konštanta -- neutrálny prvok).
    Axiómy sú:
    \begin{enumerate}
            \item $((x+y)+z) = (x+(y+z))$ -- asociativita
            \item $(x+0) = (0+x) = x$ -- existuje neutrálny prvok
            označený ako 0
            \item $x+(-x) = 0 = (-x)+x$ -- existujú (ľavé a pravé) inverzné
            prvky
    \end{enumerate}
%%% }}}
\end{priklad}

Ďalším cieľom je stotožniť dokázateľné formuly s tautológiami.

\begin{veta}[O korektnosti]
    Ak $T$ je teória v jazyku $L$ a ak formula $A$ je taká,
    že $T \provable A$, potom $T \models A$.
\end{veta}

\begin{dokaz}
%%% {{{
    Nech $A_1, A_2, \ldots, A_n\equiv A$ je odvodenie (dôkaz) formuly $A$
    z predpokladov $T$ (v teórii $T$).
    Nech $\mathcal{M}$ nech je ľubovoľný model teórie $T$ 
    (čiže platí $\mathcal{M} \models T$).
    Ukážeme (indukciou podľa dĺžky dôkazu), že 
    ak platí $\forall j<i:\mathcal{M} \models A_j$,
    potom platí aj platí $\mathcal{M} \models A_i$

    Do dôkazu sa $A_i$ môže dostať niekoľkými spôsobmi:
    \begin{enumerate}
    \item $A_i \in T, \mathcal{M}$ je model $T$. Potom 
        $\mathcal{M} \models A_i$ a teda $T \models A_i$

    \item $A_i$ sa dostane do dôkazu ako axióma predikátovej logiky:
    \begin{enumerate}
        \item $A_i$ je axióma výrokovej logiky -- je poskladaná z
            atomických formúl a logických spojok $\neg$ a $\implies$. Potom
            $A_i$ je tautológia výrokovej logiky a ak je formula tautológia,
            jej pravdivostná hodnota nezávisí od ohodnotenia
            premenných:
            $\mathcal{M} \models A_i$, čiže $\mathcal{M} \models A_i[e]$.

        \item $A_i$ je axioma špecifikácie, teda je tvaru 
            $A_i: (\forall x) B \implies B_x[t]$, kde
            $t$ je substitúcia za $x$ do $B$. 
            Chceme ukázať, že formula bude pravdivá
            pri každom ohodnotení $e$.
            Zaujíma nás prípad, kedy $(\forall x) B$ je pravdivý.\footnote{
                v opačnom prípade implikácia triviálne platí}
            To znamená, že pre ľubovoľné indivíduum $m$ platí (z Tarského
            definície) $B[e(x/m)]$, teda $e(x)=m$.
        
            Tvrdenie zo zimného semestra: Ak platí
              $\forall i: t_i[e] = m_i$, potom

            \begin{equation*}
                \mathcal{M} \models A_{x_1, \ldots x_n}[t_1, \ldots t_n][e] 
                    \iff
                \mathcal{M} \models A[e(x_1/m_1, \ldots x_n/m_n)]
            \end{equation*}

            Teda namiesto $B_x[t][e]$, vieme použiť $B[e(x/m)]$.
            Táto formula je ale pravdivá v $\mathcal{M}$ (viď vyššie).

        \item $A_i: (\forall x) (B \implies C) \implies (B \implies
            (\forall x) C)$ a $x$ nie je voľná v $B$.
            Mali by sme dokázať, že platí $\mathcal{M} \models A_i$.
            Zaujímavý prípad je, keď
            $\mathcal{M} \models (B \implies C)[e(x/m)]$ platí pre
            ľubovoľné indivíduum $m$, vtedy sa
            pozeráme na platnosť $(B \implies (\forall x)C)$.
            Posledná formula je ale ekvivalentná s $\neg B \lor (\forall x) C$.
            Dôležitý je tiež predpoklad, že $x$ nie je voľná v $B$,
            a teda $B$ nezávisí od jej ohodnotenia.
            Ak $B$ nie je pravdivá, tak disjunkcia je pravdivá a
            problém je vyriešený.
            Ak by $B$ bola pravdivá, tak by malo byť $(\forall x) C$
            pravdivé. Lenže to musí byť, inak by neplatilo
            $(\forall x) (B \implies C)$.
    \end{enumerate}

    \item $A_i$ je niektorá axióma rovnosti:
    \begin{enumerate}
        \item $A_i: x=x$. Potom $A_i[e]$ je $m=m$ a teda pri každom
            ohodnotení $\mathcal{M} \models A_i$.

        \item $A_i: (x_1 = y_1) \implies (x_2 = y_2) \implies \ldots 
            \implies [f(x_1, \ldots, x_n) = f(y_1, \ldots, y_n)]$.
            Zaujíma nás prípad, keď  $e(x_i) = e(y_i)$, teda
            $e(x_i)=e(y_i)=m_i$. Vtedy dostávame
            \begin{equation*}
              m_1=m_1 \implies m_2=m_2 \implies \ldots
                \implies [f(m_1, \dots, m_n) =f(m_1, \dots, m_n)]
            \end{equation*}

        \item $A_i: (x_1 = y_1) \implies (x_2 = y_2) \implies \ldots 
            \implies [P(x_1, \ldots, x_n) \implies P(y_1, \ldots, y_n)]$.
            Zaujíma nás opäť prípad, keď $x_i$ aj $y_i$ reprezentujeme 
            rovnakým indivíduom: $e(x_i/m_i)$ a $e(y_i/m_i)$.
            Potom $(m_1,\dots,m_n)$ buď je alebo nie je v relácii $P$
            a implikácia $P \implies P$ bude pravdivá.
    \end{enumerate}

    \item $A_i$ dostávame ako výsledok odvodzovacieho pravidla.
        \begin{enumerate}
        \item Modus Ponens:
            Vieme
            $T \provable A_j,\ T \provable A_j \implies A_i$.
            Podľa IP platí
            $T \models A_j,\ T \models A_j \implies A_i$ a vďaka
            korektnosti MP teda aj $T \models A_i$.

        \item Pravidlo zovšebecnenia: $A_i: (\forall x) A_j$.
            Z IP platí $T \models A_j $ a teda 
                $\mathcal{M} \models A_i[e(x/m)]$
            pre ľubovoľné indivíduum $m$. Tým pádom ale
            $T \models (\forall x) A_j$.
            
        \end{enumerate}
    \end{enumerate}
%%% }}}
\end{dokaz}


\begin{priklad} % existencia nedokazatelnej formuly a jej negacie v el. ar.
%%% {{{
    Uvažujme elementárnu aritmetiku, ktorá má svoj štandardný
    model $\mathcal{M}$. Uvažujme formulu $x=0$ v $N$.
    \begin{itemize}
        \item Nech $e(x) = m$ kde $m \neq 0$. Potom formula $A:x=0$ nie je
        splnená pre ohodnotenie $e$ a teda $\mathcal{M} \notmodels A[e]$.
        \item Nech $e(x) = 0$. Potom formula $A': \neg x=0$ nie je
        splnená v ohodnotení $e$, t.j. $\mathcal{M} \notmodels A'[e]$.
    \end{itemize}
    To ale znemaná, že formula $A$ ani jej negácia $A'$
    nie sú splniteľné (a teda dokázateľné) v elementárnej aritmetike.
%%% }}}
\end{priklad}


\begin{poznamka} % neexistencia vety o dedukcii v predikatovej logike
%%% {{{
    Vetu o dedukcii v predikátovej logike nemožno vysloviť pre
    ľubovoľnú formulu. Ukážeme to na nasledujúcom príklade: Majme
    formuly $A,A'$
    \begin{align*}
            A :\ & \neg x=0 \\
            A':\ & \neg y=0 \\
    \end{align*}
    $A'$ je inštancia formuly $A$. Potom ale platí:
    \begin{align*}
            A &\provable A'  \quad \mbox{čiže}\\
            \neg (x=0) &\provable \neg (y=0)
    \end{align*}
    Môžem podľa vety o dedukcii napísať, že 
    $\provable \neg (x=0) \implies \neg (y=0)$? Nie, pretože ak
    vezmeme ohodnotenie $e$ nasledovne
    \begin{align*}
        e(x) &= m, \quad m \neq 0 \\
        e(y) &= 0
    \end{align*}
    dostávame
    \begin{equation*}
        \mathcal{M} \notmodels (A \implies A')[e]
    \end{equation*}
    Dôležitým faktom je, že pri dôkaze sme totiž skryte použili
    pravidlo zovšeobecnenia na voľnú premennú $\then$ nemôžeme použiť
    VD.
%%% }}}
\end{poznamka}

\begin{dosledok}[Vety o korektnosti]
    Ak teória $T$ v jazyku $L$ má model $\mathcal{M}$, potom $T$ je
    bezosporná.
\end{dosledok}
\begin{dokaz}
%%% {{{
    Nech $\mathcal{M}$ je model $T$. Teória $T$ je tým pádom
    bezosporná. Uvažujme ďalej, že $A$ je ľubovoľná uzavretá formula jazyka $L$.
    Potom práve jedna z formúl $A$, $\neg A$ je pravdivá v modeli
    $\mathcal{M}$
    (podľa Tarského definície splniteľnosti).
    Lenže tá, ktorá nie je pravdivá, nie je ani dokázateľná 
    (podľa vety o korektnosti).
    \\
%%% }}}
\end{dokaz}

\medskip
Tento výsledok hovorí, ze ak máme vyšetriť bezospornosť nejakej teórie,
treba nájsť jej model. Dôkazy bezospornosti môžeme rozdeliť na 2 typy:
\begin{itemize}
    \item syntaktické -- sú to konečné posutpnosti symbolov, alebo
        formúl. Ak chceme dokázať bezospornosť $T$, môžeme popísať
        postup, ako dôkaz sporu v $T$ prevedieme na dôkaz sporu
        v teórii $S$, o ktorej vieme, že je bezosporná.
        Napríklad ak $T$ je predikátová logika, môžeme ju previesť na
        výrokovú logiku $S$.

    \item sémantické -- niekedy nie je možné dokazovať syntakticky.
        Sémanticky dokazujeme tak, že nájdeme potenciálne nekonečný model
        $\mathcal{M}$ teórie $T$.
\end{itemize}


\begin{priklad}[Bezospornosť predikátovej logiky]
    Ideme ukázať, že predikátová logika je bezosporná na základe toho,
    že výroková logika je bezosporná.

    Máme jazyk $L$ -- jazyk prvého rádu,
    ktorý rozšírime o konštantu $c \notin L$.
    Dostaneme tak jazyk $L' = L \union \{c\}$ zohrávajúci dôležitú
    rolu v dôkaze.

    Proces dokazovania bude prebiehať nasledovne:
    Každý term formuly $A$ nahradíme konštantou $c$,
    ďalej z danej formuly vynechávame všetky kvantifikátory a
    premenné bezprostredne spojené s kvantifikátorom.

    Každej formule $A$ na jazyku $L$ teda priradíme
    formulu $A^*$ na jazyku $L'$ nasledovne:
    \begin{enumerate}
        \item $A$ je tvaru $P(t_1, \dots ,t_n)$,
                tak $A^*: P(c, c, \dots,c)$.\footnote{
                O funkčné symboly sa nemusíme starať -- nahradili sme
                ich totiž konštntou $c$.
            }

        \item $A$ je tvaru $t_1=t_2$,
                tak $A^*: c=c$.

        \item $A$ je tvaru $B \implies C$,
                potom $A^*: B^* \implies C^*$.

        \item $A$ je tvaru $B \squareop C$,
                potom $A^*: B^* \squareop C^*$.

        \item $A$ je tvaru $\neg B$,
                potom $A^*: \neg B^*$

        \item $A$ je tvaru $(Qx) B$, potom $A^*: B^*$.
    \end{enumerate}

    Ak jazyk $L$ je jazyk bez rovnosti a $\provable_L A$, potom
    o formule $A^*$ tvrdíme, že je to tautológia.
    Na druhú stranu, ak $L$ je jazyk s rovnosťou a $\provable_L A$,
    potom $A^*$ je tautologický dôsledok $c=c$.\footnote{
        Toto sa na prvý pohľad zá byť kontraintuitívne. Majme totiž
        formulu $\exists x \exists y \neg (x=y)$. Z jej dokázateľnosti
        tvrdíme dokázateľnosť $\neg (c=c)$ čo je evidentne nepravda.

        Problém je v tom, že $\exists x \exists y \neg (x=y)$
        dokázateľná nie je. Prečo? Pozrime sa na celú našu redukciu.
        Akoby sme dosadili špeciálny model $\mathcal{M}$, ktorého
        univerzum $M$ tvorí iba jediná hodnota -- konštanta $c$.
        Teda, ak pôvodná formula bola dokázateľná $\then$ platí v
        každom modeli, teda špeciálne aj našom. Lenže v našom modeli
        sa interpretuje ako $\neg (c=c)$ a teda nemohla byť
        dokázateľná.
    }

    Teraz ukážeme, že predikátová logika nie je sporná:
    Tvrdíme, že pre žiadnu formulu $A$ nie je $\provable A$ aj 
    $\provable \neg A$.
    Ak by to platilo, dostali by sme sa do sporu,
    že vo výrokovej logike je $\provable A^*$ aj $\provable \neg A^*$.
\end{priklad}
